package org.eclipse.iota.util;

import java.util.ArrayList;
import java.util.List;

import org.eclipse.iota.model.Alternation;
import org.eclipse.iota.model.Definition;
import org.eclipse.iota.model.Element;
import org.eclipse.iota.model.Parameter;
import org.eclipse.iota.model.Proof;
import org.eclipse.iota.model.Proof.ProofException;
import org.eclipse.iota.model.Property;
import org.eclipse.iota.model.Sequent;
import org.eclipse.iota.model.Step;
import org.eclipse.iota.rewrite.IotaRule;
import org.eclipse.iota.rewrite.IotaRuleManager;
import org.eclipse.iota.rewrite.IotaRuleMatchFinder;

/**
 * Iota proof assistant methods.
 * @author Christian Krause
 * @generated NOT
 */
public class IotaProofAssistant {
	
	/**
	 * For a given property, find a list of all applicable proof steps.
	 * @param property Property.
	 * @return List of steps.
	 */
	public static List<Step> getApplicableSteps(Property property, String ruleNamePrefix) {
		
		// Some preparations....
		if (ruleNamePrefix==null) ruleNamePrefix = "";
		ruleNamePrefix = ruleNamePrefix.toLowerCase();
		List<Step> steps = new ArrayList<Step>();

		// Try out all registered rules:
		for (Class<? extends IotaRule> type : IotaRuleManager.INSTANCE.getRuleTypes()) {
			IotaRule rule = IotaRuleManager.newInstance(type);
			String name = rule.getName();
			if (name!=null && name.toLowerCase().startsWith(ruleNamePrefix)) {
				Property copy = IotaCopyUtil.copy(property);
				for (Element target : IotaRuleMatchFinder.findMatches(rule, copy)) {
					steps.add(new Step(rule, target.toString(), 0));
				}
			}
		}
		return steps;
		
	}
	
	/**
	 * Get the intermediate result of a proof.
	 * @param sequent Sequent.
	 * @param until Index of the last step to be used.
	 * @return The intermediate result as a property
	 * @throws ProofException On proof errors.
	 */
	public static Property getIntermediateResult(Sequent sequent, int until) throws ProofException {
		if (sequent==null || sequent.getPremise()==null || sequent.getProof()==null) {
			throw new NullPointerException("Invalid sequent");
		}
		Proof proof = sequent.getProof();
		Property property = getPremiseAsProperty(sequent);
		until = Math.min(until, proof.getSteps().size());
		for (int i=0; i<=until; i++) {
			try {
				proof.getSteps().get(i).apply(property.getBody(), true);
			} catch (ProofException e) {
				throw e;
			} catch (Throwable t) {
				throw new ProofException(t.getMessage(), null, t);
			}
		}
		return property;
	}
	
	/**
	 * Get the premise of a sequent as a fresh, self-contained property.
	 * @param sequent The sequent.
	 * @return The fresh property.
	 */
	public static Property getPremiseAsProperty(Sequent sequent) {
		return alternationToProperty(sequent.getPremise());
	}

	/**
	 * Get the conclusion of a sequent as a fresh, self-contained property.
	 * @param sequent The sequent.
	 * @return The fresh property.
	 */
	public static Property getConclusionAsProperty(Sequent sequent) {
		return alternationToProperty(sequent.getConclusion());
	}

	/*
	 * Copy an alternation including its parameters and wrap it in a property.
	 */
	private static Property alternationToProperty(Alternation alternation) {
		if (alternation==null || alternation.getDefinition()==null) {
			return null;
		}
		Definition copy = IotaCopyUtil.copy(alternation.getDefinition());
		Property property = new Property(copy.getName(), copy.getParameters().toArray(new Parameter[0]));
		property.setBody((Alternation) copy.eGet(alternation.eContainingFeature()));
		return property;
	}
	
}
